Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    pred(s(x))  → x
2:    minus(x,0)  → x
3:    minus(x,s(y))  → pred(minus(x,y))
4:    quot(0,s(y))  → 0
5:    quot(s(x),s(y))  → s(quot(minus(x,y),s(y)))
There are 4 dependency pairs:
6:    MINUS(x,s(y))  → PRED(minus(x,y))
7:    MINUS(x,s(y))  → MINUS(x,y)
8:    QUOT(s(x),s(y))  → QUOT(minus(x,y),s(y))
9:    QUOT(s(x),s(y))  → MINUS(x,y)
The approximated dependency graph contains 2 SCCs: {7} and {8}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006